\begin{tabbing}
$\forall$\=${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $n$:$\mathbb{N}$, $v$:ecl{-}trans{-}tuple\{i:l\}(${\it ds}$; ${\it da}$),\+
\\[0ex]$L$:(event{-}info(${\it ds}$;${\it da}$) List), $m$:$\mathbb{N}$.
\-\\[0ex](ecl{-}trans{-}halt2(${\it ds}$; ${\it da}$; ecl{-}add{-}throw($v$; $n$))($m$,$L$))
\\[0ex]$\Leftarrow\!\Rightarrow$ \=((($n$ = $m$ $\in$ $\mathbb{Z}$)\+
\\[0ex]$\wedge$ ((ecl{-}trans{-}halt2(${\it ds}$; ${\it da}$; $v$)(0,$L$)) $\vee$ (ecl{-}trans{-}halt2(${\it ds}$; ${\it da}$; $v$)($m$,$L$))))
\\[0ex]$\vee$ (($\neg$($n$ = $m$ $\in$ $\mathbb{Z}$)) $\wedge$ (0 $<$ $m$) $\wedge$ (ecl{-}trans{-}halt2(${\it ds}$; ${\it da}$; $v$)($m$,$L$))))
\-
\end{tabbing}